T:Type, R, R':(TT). (R <>{T} R')  (order(T;R)  order(T;R')) 

latex

Up	gen algebra 1
Definitions of Statement	order(T;R)
Definitions	t  T, P  Q, P & Q, order(T;R), P  Q, P  Q, , x:A. B(x)
Lemmas	binrel eqv wf, xxanti sym functionality wrt breqv, xxtrans functionality wrt breqv, xxrefl functionality wrt breqv, and functionality wrt iff, xxanti sym wf, xxtrans wf, xxrefl wf, iff functionality wrt iff